\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage{listings}
\usepackage{oz, amsfonts}
\usepackage{graphicx}

\title{Software Engineering\\Assignment 5}
\author{Adrian.Nembach@uni-konstanz.de 01/842319\\Udo.3.Schlegel@uni-konstanz.de 01/840835\\Sirui.Liu@uni-konstanz.de 01/857316}
\begin{document}
\maketitle

\section*{Exercise 6.1}
\begin{verbatim}
mtype = {digits, onhook, busy };

chan ptp = [0] of { mtype };

active [2] proctype phone()
{
Idle:
            if
            :: printf("off_hook\n"); goto Waiting;
            :: ptp?digits ->
                    printf("ringing\n"); goto Ringing;
            fi;

Waiting:
            if
            :: printf("audible_dialtone\n"); goto Enter_tone;
            :: printf("audible_busytone\n"); goto Busy;
            :: printf("on_hook\n"); goto Idle;
            fi;

Busy:
            if
            :: printf("on_hook\n"); goto Idle;
            fi;

Enter_tone:
            if
            :: printf("call_number\n"); goto Calling;
            :: printf("on_hook\n"); goto Idle;
            fi;

Calling:
            if
            :: ptp?busy ->
                    printf("callee_line_busy\n"); goto Busy;
            :: ptp!digits ->
                    printf("audible_ring\n"); goto Waiting_for_callee;
            :: printf("on_hook\n"); goto Idle;
            fi;

Waiting_for_callee:
            if
            :: printf("timeout\n"); goto Busy;
            :: printf("callee_off_hook\n"); goto Conversation;
            :: printf("on_hook\n"); goto Idle;
            fi;

Conversation:
            if
            :: ptp!onhook ->
                    printf("on_hook\n"); goto Idle;
            :: ptp?onhook ->
                    printf("on_hook\n"); goto Idle;
            fi;

Ringing:
            if
            :: printf("timeout\n"); goto Idle;
            :: printf("off_hook\n"); goto Conversation;
            fi;
}
\end{verbatim}
\section*{Exercise 6.2}
\begin{lstlisting}
{true}

if x >= y
  //{true & x >= y} -> {x >= y}
  then x := x - y  
  //Q1: {x := x-y & x >= y}
  							
  //{true & not(x >= y)} -> {x < y}
  else x := y - x  
  //Q2: {x < y & x := y - x}
  
{x >= 0}			  
//{Q1 || Q2} -> Q
//Q = {x := x-y & x >= y} || {x < y & x := y - x} => Q = {x >= 0}
\end{lstlisting}
\end{document}